On the complexity of choosing the branching literal in DPLL

摘要

The DPLL (Davis-Putnam-Logemann-Loveland) algorithm is one of the best-known algorithms for solving the problem of satisfiability of propositional formulas. Its efficiency is affected by the way:literals to branch on are chosen. In this paper we analyze the Complexity of the problem of choosing an optimal literal. Namely, we prove that this problem is both NP-hard and coNP-hard, and is in PSPACE. We also study its approximability. (C) 2000 Elsevier Science B.V. All rights reserved.